The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

f(f(X)) → c(n__f(n__g(n__f(X))))
c(X) → d(activate(X))
h(X) → c(n__d(X))
f(X) → n__f(X)
g(X) → n__g(X)
d(X) → n__d(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(X)
activate(n__d(X)) → d(X)
activate(X) → X

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

f(f(X)) → c(n__f(n__g(n__f(X)))) [1]
c(X) → d(activate(X)) [1]
h(X) → c(n__d(X)) [1]
f(X) → n__f(X) [1]
g(X) → n__g(X) [1]
d(X) → n__d(X) [1]
activate(n__f(X)) → f(activate(X)) [1]
activate(n__g(X)) → g(X) [1]
activate(n__d(X)) → d(X) [1]
activate(X) → X [1]

Rewrite Strategy: INNERMOST

(3) InnermostUnusableRulesProof (BOTH BOUNDS(ID, ID) transformation)

Removed the following rules with non-basic left-hand side, as they cannot be used in innermost rewriting:

f(f(X)) → c(n__f(n__g(n__f(X)))) [1]

Due to the following rules that have to be used instead:

f(X) → n__f(X) [1]

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

c(X) → d(activate(X)) [1]
h(X) → c(n__d(X)) [1]
f(X) → n__f(X) [1]
g(X) → n__g(X) [1]
d(X) → n__d(X) [1]
activate(n__f(X)) → f(activate(X)) [1]
activate(n__g(X)) → g(X) [1]
activate(n__d(X)) → d(X) [1]
activate(X) → X [1]

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

c(X) → d(activate(X)) [1]
h(X) → c(n__d(X)) [1]
f(X) → n__f(X) [1]
g(X) → n__g(X) [1]
d(X) → n__d(X) [1]
activate(n__f(X)) → f(activate(X)) [1]
activate(n__g(X)) → g(X) [1]
activate(n__d(X)) → d(X) [1]
activate(X) → X [1]

The TRS has the following type information:

c :: n__d:n__f:n__g → n__d:n__f:n__g d :: n__d:n__f:n__g → n__d:n__f:n__g activate :: n__d:n__f:n__g → n__d:n__f:n__g h :: n__d:n__f:n__g → n__d:n__f:n__g n__d :: n__d:n__f:n__g → n__d:n__f:n__g f :: n__d:n__f:n__g → n__d:n__f:n__g n__f :: n__d:n__f:n__g → n__d:n__f:n__g g :: a → n__d:n__f:n__g n__g :: a → n__d:n__f:n__g

Rewrite Strategy: INNERMOST

(7) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

c
h

(c) The following functions are completely defined:

activate
d
f
g

Due to the following rules being added:
none

And the following fresh constants:

const, const1

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: c(X) → d(activate(X)) [1] h(X) → c(n__d(X)) [1] f(X) → n__f(X) [1] g(X) → n__g(X) [1] d(X) → n__d(X) [1] activate(n__f(X)) → f(activate(X)) [1] activate(n__g(X)) → g(X) [1] activate(n__d(X)) → d(X) [1] activate(X) → X [1] The TRS has the following type information: c :: n__d:n__f:n__g → n__d:n__f:n__g d :: n__d:n__f:n__g → n__d:n__f:n__g activate :: n__d:n__f:n__g → n__d:n__f:n__g h :: n__d:n__f:n__g → n__d:n__f:n__g n__d :: n__d:n__f:n__g → n__d:n__f:n__g f :: n__d:n__f:n__g → n__d:n__f:n__g n__f :: n__d:n__f:n__g → n__d:n__f:n__g g :: a → n__d:n__f:n__g n__g :: a → n__d:n__f:n__g const :: n__d:n__f:n__g const1 :: a Rewrite Strategy: INNERMOST

(9) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(10) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: c(n__f(X')) → d(f(activate(X'))) [2] c(n__g(X'')) → d(g(X'')) [2] c(n__d(X1)) → d(d(X1)) [2] c(X) → d(X) [2] h(X) → c(n__d(X)) [1] f(X) → n__f(X) [1] g(X) → n__g(X) [1] d(X) → n__d(X) [1] activate(n__f(n__f(X2))) → f(f(activate(X2))) [2] activate(n__f(n__g(X3))) → f(g(X3)) [2] activate(n__f(n__d(X4))) → f(d(X4)) [2] activate(n__f(X)) → f(X) [2] activate(n__g(X)) → g(X) [1] activate(n__d(X)) → d(X) [1] activate(X) → X [1] The TRS has the following type information: c :: n__d:n__f:n__g → n__d:n__f:n__g d :: n__d:n__f:n__g → n__d:n__f:n__g activate :: n__d:n__f:n__g → n__d:n__f:n__g h :: n__d:n__f:n__g → n__d:n__f:n__g n__d :: n__d:n__f:n__g → n__d:n__f:n__g f :: n__d:n__f:n__g → n__d:n__f:n__g n__f :: n__d:n__f:n__g → n__d:n__f:n__g g :: a → n__d:n__f:n__g n__g :: a → n__d:n__f:n__g const :: n__d:n__f:n__g const1 :: a Rewrite Strategy: INNERMOST

(11) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

const => 0
const1 => 0

(12) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ g(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ f(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ f(g(X3)) :|: z = 1 + (1 + X3), X3 >= 0
activate(z) -{ 2 }→ f(f(activate(X2))) :|: z = 1 + (1 + X2), X2 >= 0
activate(z) -{ 2 }→ f(d(X4)) :|: z = 1 + (1 + X4), X4 >= 0
activate(z) -{ 1 }→ d(X) :|: z = 1 + X, X >= 0
c(z) -{ 2 }→ d(X) :|: X >= 0, z = X
c(z) -{ 2 }→ d(g(X'')) :|: z = 1 + X'', X'' >= 0
c(z) -{ 2 }→ d(f(activate(X'))) :|: X' >= 0, z = 1 + X'
c(z) -{ 2 }→ d(d(X1)) :|: X1 >= 0, z = 1 + X1
d(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
f(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
g(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
h(z) -{ 1 }→ c(1 + X) :|: X >= 0, z = X

(13) InliningProof (UPPER BOUND(ID) transformation)

Inlined the following terminating rules on right-hand sides where appropriate:

f(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
g(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
d(z) -{ 1 }→ 1 + X :|: X >= 0, z = X

(14) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ f(f(activate(X2))) :|: z = 1 + (1 + X2), X2 >= 0
activate(z) -{ 3 }→ f(1 + X) :|: z = 1 + (1 + X3), X3 >= 0, X >= 0, X3 = X
activate(z) -{ 3 }→ f(1 + X) :|: z = 1 + (1 + X4), X4 >= 0, X >= 0, X4 = X
activate(z) -{ 3 }→ 1 + X' :|: z = 1 + X, X >= 0, X' >= 0, X = X'
activate(z) -{ 2 }→ 1 + X' :|: z = 1 + X, X >= 0, X' >= 0, X = X'
c(z) -{ 2 }→ d(f(activate(X'))) :|: X' >= 0, z = 1 + X'
c(z) -{ 4 }→ 1 + X' :|: X1 >= 0, z = 1 + X1, X >= 0, X1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + X' :|: X >= 0, z = X, X' >= 0, X = X'
c(z) -{ 4 }→ 1 + X' :|: z = 1 + X'', X'' >= 0, X >= 0, X'' = X, X' >= 0, 1 + X = X'
d(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
f(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
g(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
h(z) -{ 1 }→ c(1 + X) :|: X >= 0, z = X

(15) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(16) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ f(f(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ f(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 2 }→ d(f(activate(z - 1))) :|: z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

(17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ g } { f } { d } { activate } { c } { h }

(18) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ f(f(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ f(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 2 }→ d(f(activate(z - 1))) :|: z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {g}, {f}, {d}, {activate}, {c}, {h}

(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: g
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(20) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ f(f(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ f(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 2 }→ d(f(activate(z - 1))) :|: z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {g}, {f}, {d}, {activate}, {c}, {h}
Previous analysis results are:

g: runtime: ?, size: O(n1) [1 + z]

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: g
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(22) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ f(f(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ f(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 2 }→ d(f(activate(z - 1))) :|: z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {f}, {d}, {activate}, {c}, {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z]

(23) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(24) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ f(f(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ f(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 2 }→ d(f(activate(z - 1))) :|: z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {f}, {d}, {activate}, {c}, {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z]

(25) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: f
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(26) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ f(f(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ f(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 2 }→ d(f(activate(z - 1))) :|: z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {f}, {d}, {activate}, {c}, {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: ?, size: O(n1) [1 + z]

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: f
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(28) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ f(f(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ f(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 2 }→ d(f(activate(z - 1))) :|: z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {d}, {activate}, {c}, {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: O(1) [1], size: O(n1) [1 + z]

(29) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(30) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ f(f(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 2 }→ d(f(activate(z - 1))) :|: z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {d}, {activate}, {c}, {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: O(1) [1], size: O(n1) [1 + z]

(31) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: d
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(32) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ f(f(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 2 }→ d(f(activate(z - 1))) :|: z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {d}, {activate}, {c}, {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: O(1) [1], size: O(n1) [1 + z] d: runtime: ?, size: O(n1) [1 + z]

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: d
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(34) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ f(f(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 2 }→ d(f(activate(z - 1))) :|: z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {activate}, {c}, {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: O(1) [1], size: O(n1) [1 + z] d: runtime: O(1) [1], size: O(n1) [1 + z]

(35) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(36) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ f(f(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 2 }→ d(f(activate(z - 1))) :|: z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {activate}, {c}, {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: O(1) [1], size: O(n1) [1 + z] d: runtime: O(1) [1], size: O(n1) [1 + z]

(37) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: activate
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(38) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ f(f(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 2 }→ d(f(activate(z - 1))) :|: z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {activate}, {c}, {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: O(1) [1], size: O(n1) [1 + z] d: runtime: O(1) [1], size: O(n1) [1 + z] activate: runtime: ?, size: O(n1) [z]

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: activate
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 10 + 4·z

(40) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ f(f(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 2 }→ d(f(activate(z - 1))) :|: z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {c}, {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: O(1) [1], size: O(n1) [1 + z] d: runtime: O(1) [1], size: O(n1) [1 + z] activate: runtime: O(n1) [10 + 4·z], size: O(n1) [z]

(41) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(42) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 6 + 4·z }→ s1 :|: s' >= 0, s' <= 1 * (z - 2), s'' >= 0, s'' <= 1 * s' + 1, s1 >= 0, s1 <= 1 * s'' + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 10 + 4·z }→ s4 :|: s2 >= 0, s2 <= 1 * (z - 1), s3 >= 0, s3 <= 1 * s2 + 1, s4 >= 0, s4 <= 1 * s3 + 1, z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {c}, {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: O(1) [1], size: O(n1) [1 + z] d: runtime: O(1) [1], size: O(n1) [1 + z] activate: runtime: O(n1) [10 + 4·z], size: O(n1) [z]

(43) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: c
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(44) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 6 + 4·z }→ s1 :|: s' >= 0, s' <= 1 * (z - 2), s'' >= 0, s'' <= 1 * s' + 1, s1 >= 0, s1 <= 1 * s'' + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 10 + 4·z }→ s4 :|: s2 >= 0, s2 <= 1 * (z - 1), s3 >= 0, s3 <= 1 * s2 + 1, s4 >= 0, s4 <= 1 * s3 + 1, z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {c}, {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: O(1) [1], size: O(n1) [1 + z] d: runtime: O(1) [1], size: O(n1) [1 + z] activate: runtime: O(n1) [10 + 4·z], size: O(n1) [z] c: runtime: ?, size: O(n1) [1 + z]

(45) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: c
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 17 + 4·z

(46) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 6 + 4·z }→ s1 :|: s' >= 0, s' <= 1 * (z - 2), s'' >= 0, s'' <= 1 * s' + 1, s1 >= 0, s1 <= 1 * s'' + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 10 + 4·z }→ s4 :|: s2 >= 0, s2 <= 1 * (z - 1), s3 >= 0, s3 <= 1 * s2 + 1, s4 >= 0, s4 <= 1 * s3 + 1, z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 1 }→ c(1 + z) :|: z >= 0

Function symbols to be analyzed: {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: O(1) [1], size: O(n1) [1 + z] d: runtime: O(1) [1], size: O(n1) [1 + z] activate: runtime: O(n1) [10 + 4·z], size: O(n1) [z] c: runtime: O(n1) [17 + 4·z], size: O(n1) [1 + z]

(47) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(48) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 6 + 4·z }→ s1 :|: s' >= 0, s' <= 1 * (z - 2), s'' >= 0, s'' <= 1 * s' + 1, s1 >= 0, s1 <= 1 * s'' + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 10 + 4·z }→ s4 :|: s2 >= 0, s2 <= 1 * (z - 1), s3 >= 0, s3 <= 1 * s2 + 1, s4 >= 0, s4 <= 1 * s3 + 1, z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 22 + 4·z }→ s5 :|: s5 >= 0, s5 <= 1 * (1 + z) + 1, z >= 0

Function symbols to be analyzed: {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: O(1) [1], size: O(n1) [1 + z] d: runtime: O(1) [1], size: O(n1) [1 + z] activate: runtime: O(n1) [10 + 4·z], size: O(n1) [z] c: runtime: O(n1) [17 + 4·z], size: O(n1) [1 + z]

(49) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: h
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + z

(50) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 6 + 4·z }→ s1 :|: s' >= 0, s' <= 1 * (z - 2), s'' >= 0, s'' <= 1 * s' + 1, s1 >= 0, s1 <= 1 * s'' + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 10 + 4·z }→ s4 :|: s2 >= 0, s2 <= 1 * (z - 1), s3 >= 0, s3 <= 1 * s2 + 1, s4 >= 0, s4 <= 1 * s3 + 1, z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 22 + 4·z }→ s5 :|: s5 >= 0, s5 <= 1 * (1 + z) + 1, z >= 0

Function symbols to be analyzed: {h}
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: O(1) [1], size: O(n1) [1 + z] d: runtime: O(1) [1], size: O(n1) [1 + z] activate: runtime: O(n1) [10 + 4·z], size: O(n1) [z] c: runtime: O(n1) [17 + 4·z], size: O(n1) [1 + z] h: runtime: ?, size: O(n1) [2 + z]

(51) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: h
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 22 + 4·z

(52) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 6 + 4·z }→ s1 :|: s' >= 0, s' <= 1 * (z - 2), s'' >= 0, s'' <= 1 * s' + 1, s1 >= 0, s1 <= 1 * s'' + 1, z - 2 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
c(z) -{ 10 + 4·z }→ s4 :|: s2 >= 0, s2 <= 1 * (z - 1), s3 >= 0, s3 <= 1 * s2 + 1, s4 >= 0, s4 <= 1 * s3 + 1, z - 1 >= 0
c(z) -{ 4 }→ 1 + X' :|: z - 1 >= 0, X >= 0, z - 1 = X, X' >= 0, 1 + X = X'
c(z) -{ 3 }→ 1 + z :|: z >= 0
d(z) -{ 1 }→ 1 + z :|: z >= 0
f(z) -{ 1 }→ 1 + z :|: z >= 0
g(z) -{ 1 }→ 1 + z :|: z >= 0
h(z) -{ 22 + 4·z }→ s5 :|: s5 >= 0, s5 <= 1 * (1 + z) + 1, z >= 0

Function symbols to be analyzed:
Previous analysis results are:

g: runtime: O(1) [1], size: O(n1) [1 + z] f: runtime: O(1) [1], size: O(n1) [1 + z] d: runtime: O(1) [1], size: O(n1) [1 + z] activate: runtime: O(n1) [10 + 4·z], size: O(n1) [z] c: runtime: O(n1) [17 + 4·z], size: O(n1) [1 + z] h: runtime: O(n1) [22 + 4·z], size: O(n1) [2 + z]

(53) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(54) BOUNDS(1, n^1)